\section{Veta o úplnosti}

G\"odelova veta, ktorú si teraz vyslovíme a dokážeme, má 2 varianty.

\begin{veta}[G\"odel, 1. variant]
    Nech $T$ je teória v jazyku $L$ a nech $A$ je
    ľubovoľná formula jazyka $L$. Potom $T \provable A \iff T \models A$,
    čiže $A$ je dokázateľná práve vtedy keď
    je splnená v každom modeli teórie $T$.
\end{veta}

\begin{veta}[G\"odel, 2. variant]
    Teória $T$ je bezosporná práve vtedy, ked $T$ má model.
\end{veta}

\begin{poznamka}
    Varianta 1 G\"odelovej vety vyplýva z variantu 2.
\end{poznamka}

\begin{dokaz}[Poznámky]
    Veta o dedukcii mala nasledovný dôsledok:

    Majme teóriu $T$ a jej formulu $A$. Nech $A'$ označuje uzáver
    formuly $A$.
    Potom platí: $T \provable A \iff T \union \{ \neg A' \}$ je sporná
    teória.

    V našom prípade z 2. varianty G\"odelovej vety dostávame
    $T \provable A \iff T \union \{ \neg A' \}$ nemá model.
    Toto znamená, že v každom modeli teórie $T$ je pravdivý uzáver $A'$.
    Z toho dostávame $T \models A' \Rightarrow T \models A$
    (ak zoberieme ľubovoľný model $\mathcal{M}$ teórie $T$, formula
    $A'$ je v ňom splnená ale to nutne znamená, že aj formula $A$ v
    ňom musí byť splnená)
    a teda z platnosti variantu 2 vyplýva variant 1.
    \\
\end{dokaz}

\begin{dokaz}[2. variantu G\"odelovej vety]
    Budeme sa snažiť zostrojiť model pre teóriu, ktorá je bezosporná.
    Majme bezospornú teóriu s jazykom $L$.
    Potrebujeme v prvom rade univerzum -- $M$.
    K dispozícii máme len syntaktické prostriedky teórie.
    Preto ako kandidát na $M$ prichádza do úvahy
    množina termov bez premenných.
    Tieto termy majú jednoznačnú realizáciu (sami sebe budú
    realizáciou).\footnote{
        Pre ujasnenie tejto myšlienky odporúčame čitateľovi
        nalistovať si kapitolu o Herbrandovských interpretáciach
        a nahliadnuť tak pointu tohoto činu.
    }
    V našom modeli budú teda všetky objekty teórie charakterizované termami.

    Ďalšou otázkou je, ako definovať splniteľnosť. Malo by platiť, že
    formula je splniteľná práve vtedy keď je dokázateľná, čize
    \begin{equation*}
    A[e] \iff T \provable A
    \end{equation*}

    Pri konštrukcii modelu sa nám pritrafia isté nepríjemnosti, ktoré bude 
    treba riešiť:
    \begin{enumerate}
    \item \label{en:model_problem_konst}
        Jazyk $L$ nemusí obsahovať žiadne konštanty (a teda žiadne termy bez
        premenných).

    \item \label{en:model_problem_rovnost}
        Ak jazyk $L$ bude jazyk s rovnosťou, môže sa stať, že v teórii $T$
        bude $T \provable t=s$, ale $t$ a $s$ sú rôzne termy bez
        premenných (rôzne konštanty).

    \item \label{en:model_problem_neg}
        Nech $\mathcal{M}$ je ľubovoľná realizácia jazyka $L$ a $A$ je uzavretá
        formula jazyka $L$. Potom práve jedna z formúl $A$, $\neg A$ je
        pravdivá, ale žiadna z nich nemusí byť dokázateľná v $T$.

    \item \label{en:model_problem_korektnost}
        Môže sa stať, že uzavretá formula $(\exists x)B$ je dokázateľná v teórii
        $T$, ale pre žiaden term $t$ bez premenných formula $B_x[t]$ nie
        je dokázateľná v $T$. To znamená, že
        podľa Tarského definície pravdivosti je $(\exists x)B$
        nepravdivá, čo je spor s vetou o korektnosti.
    \end{enumerate}

    Ako odstránime tieto nedostatky?
    Odstránenie bodu \ref{en:model_problem_rovnost} je jednoduché --
    riešime vhodnou faktorizáciou, čiže zavedieme si množinu $\tau$,
    čo je množina všetkých termov bez premenných
    a na nej zavedieme reláciu ekvivalencie.

    Body č. \ref{en:model_problem_konst}, \ref{en:model_problem_neg} a 
    \ref{en:model_problem_korektnost} sa riešia tzv.
    úplným konzervatívnym rošírením teórie (Henkinovským).
    Budú to tzv.  konzervatívne teórie (na pôvodnom jazyku
    nezískame žiadne nové teorémy a ani nestratíme žiadne).
    Nachvíľu teda opustíme dôkaz G\"odelovej vety, aby sme si mohli niečo
    porozprávať o Henkinovej teórii. K dôkazu sa vrátime, keď na to budeme
    mať pripravenú pôdu.
    \\
\end{dokaz}

\begin{definicia}[Úplná teória]
%%% {{{
    Hovoríme, že teória $T$ s jazykom $L$ je úplná, ak $T$ je
    bezosporná teória a pre ľubovoľnú {\tt uzavretú} formulu $A$ na jazyku
    $L$ platí, že buď $A$ alebo $\neg A$ je dokázateľná v $T$.
%%% }}}
\end{definicia}

\begin{poznamka}
    Pojem úplnosti teda zodpovedá nasledujúcej konštrukcii:
    Majme teóriu $T$ nad jazykom $L$ a jej model $\mathcal{M}$.
    Model $\mathcal{M}$ rozhoduje o pravdivosti každej uzavretej
    formuly.
    Označme ako $T_h(\mathcal{M})$ množinu všetkých
    pravdivých uzavretých formúl $T$.
    Potom platí, že $T_h(\mathcal{M})$ je úplná.

    Je dôležité si uvedomiť, že neberieme otvorené formuly --
    napr. formula $x=0$ v elementárnej aritmetike nemusí byť pradivá, 
    pretože závisí od ohodnotenia $x$.
\end{poznamka}

\begin{poznamka}
    V úplnej teórii (a teda špeciálne v $T_h$) nemôže nastať problém 
    \ref{en:model_problem_neg}, ktorý sme spomínali.
\end{poznamka}

\begin{definicia}[Henkinova teória]
%%% {{{ Henkinova teoria
    Hovoríme, že teória $T$ s jazykom $L$ je Henkinova, ak pre
    ľubovoľnú uzavretú formulu $(\exists x)B$ jazyka $L$ platí
    \begin{equation*}
        T \provable (\exists x)B \implies B_x[c]
    \end{equation*}
    pre nejakú konštantu $c$.
%%% }}}
\end{definicia}

\begin{poznamka}
    Ak je teória Henkinova, tak sme vyriešili problémy
    \ref{en:model_problem_konst}, \ref{en:model_problem_korektnost}.
\end{poznamka}

\begin{lema}
    Ak $T$ je úplná a Henkinova teória, tak potom $T$ má model.
    \label{lema:uplna_henkinova}
\end{lema}
\begin{dokaz}
    Nech $L$ je jazyk teórie $T$ a nech $\tau$ je množina všetkých
    termov jazyka $L$ bez premenných. Na množine $\tau$ definujeme reláciu
    ekvivalencie nasledovne:
    \begin{equation*}
        \forall t_1, t_2 \in \tau :
            t_1 \equiv t_2 \iff T \provable t_1 = t_2
    \end{equation*}
    Rovnosť je reflexívna, symetrická, tranzitívna, teda týmto
    spôsobom definovaná relácia je relácia ekvivalencie a rozdeľuje
    nám množinu $\tau$ na triedy ekvivalencie:
    \begin{equation*}
        [t] = \{ s \in \tau | t \equiv s\}
    \end{equation*}
    Týmto sme vyriešili problém \ref{en:model_problem_rovnost}.

    Zadefinujme si univerzum $M$ tak, že ho budú tvoriť vyššie popísané
    triedy ekvivalencie.
    Nech $f$ je ľubovoľný $n$-árny funkčný symbol a nech
    $[t_1], [t_2], \ldots, [t_n] \in M$. Definujeme funkciu $f$ v relačnej
    štruktúre $\mathcal{M}$ nasledovne:
    \begin{equation*}
        f_\mathcal{M}([t_1], \dots, [t_n]) = [f(t_1, \dots t_n)]
    \end{equation*}
    Bolo by potrebné ukázať, že táto definícia je konzistentná. Teda,
    že platí
    $f_\mathcal{M}([t_1], \dots, [t_n])=f_\mathcal{M}([s_1], \dots, [s_n])$
    za predpokladu $\forall i \in {1,\dots,n}:s_i \equiv t_i$.
    Inak povedané, nesmie záležať na výbere reprezentantov.
    Taktiež je dobré si uvedomiť, že
    $[t_{x_1,\dots,x_n}[t_1,\dots,t_n]]=t[e]$, ak platí $e(x_i/t_i)$ resp.
    $e(x_i)=t_i$.

    Podobne, nech $P$ je $n$-árny predikátový symbol rôzny od `='
    (predikát `=' sme si už zaviedli). V tom prípade definujeme
    \begin{equation*}
     ([t_1], \dots, [t_n]) \in P_\mathcal{M} \iff
        T \provable P(t_1, \dots, t_n)
    \end{equation*}
    Zostáva nám ukázať, že nami definované $\mathcal{M}$ je
    naozaj modelom teórie $T$, čo bude predmetom nasledujúcej vety.
    \\
\end{dokaz}

\begin{veta}[O kanonickej štruktúre]
    Nech $T$ je úplná Henkinovská teória a nech $\mathcal{M}$ je
    definované podľa dôkazu lemy \ref{lema:uplna_henkinova}.
    Potom $T \provable A \iff \mathcal{M} \models A$.
\end{veta}

\begin{dokaz}
    Budeme postupovať matematickou indukciou vzhľadom na zložitosť
    formuly. Pri dokazovaní sa ale obmedzíme iba na uzavreté formuly.
    \begin{itemize}
    \item[1:] Báza indukcie:
        \begin{itemize}
        \item Formula $A$ je tvaru $P(t_1,\dots,t_n)$. Pritom $t_1,
            \dots t_n$ sú termy bez premenných (inak by formula $A$
            nebola uzavretá). Podľa definície splniteľnosti platí, že
            $A$ je pravdivá v $T$ práve vtedy keď je dokázateľná v
            $T$. Zoberme si teraz ohodnotenie $e$ také, že
            $t_i[e] = t_i$ (Čiže každý term realizujeme samým sebou).
            Podľa definície je uzavretá formula $A$ pravdivá práve vtedy, 
            keď je splnená aspoň pre jedno ohodnotenie $e$ (vtedy je
            automaticky splnená pre všetky ohodnotenia $e$).
            Teda
            \begin{equation*}
            \begin{split}
                \mathcal{M} \models A 
                &\iff \mathcal{M} \models A[e] \\
                &\iff (t_1[e],t_2[e],\dots,t_n[e]) \in P_\mathcal{M}
                \\
                &\iff ([t_1],[t_2],\dots,[t_n]) \in P_\mathcal{M} \\
                &\iff T \provable P(t_1,t_2, \dots, t_n) \equiv A
            \end{split}
            \end{equation*}

        \item Formula môže byť tvaru $A:t_1=t_2$. V tom prípade
            $\mathcal{M} \models t_1 = t_2 \iff [t_1]=[t_2] \iff
                T \provable t_1=t_2$
        \end{itemize}

    \item[2:] Indukčný krok:\\
        Máme niekoľko možností, ako mohla formula $A$ vzniknúť:
        \begin{itemize}
        \item $A:\neg B$. Na formulu $B$ sa vzťahuje IP, keďže $B$ je
            uzavretá formula. Teda
            $\mathcal{M} \models A \iff \mathcal{M} \not \models B$.
            Vieme, že teória $T$ je úplná, že buď $T \provable A$
            alebo $T \provable B$. Keďže je bezosporná, platí práve
            jedna možnosť. Tým sme ale ukázali, že
            $\mathcal{M} \models A \iff T \provable A$.

        \item $A: B \implies C$. Na formuly $B,C$ sa vzťahuje IP.
            Rozoberme si obe implikácie tvrdenia
            $\mathcal{M} \models B \implies C \iff
             T \provable B \implies C$.
            \begin{itemize}
            \item[$\Rightarrow:$] Vieme, že $(B \implies C)
                    \lequiv \neg B \lor C$. Čiže môžeme
                    predpokladať, že aspoň 1 z tvrdení 
                    $\mathcal{M} \models \neg B$,
                    $\mathcal{M} \models C$ platí. Rozoberme obe
                    možnosti -- pri prvej predpokladáme, že $\neg B$ je
                    pravdivá (a z IP dokázateľná\footnote{
                        Presnejšie povedané, IP nestačí, potrebujeme
                        spraviť ešte ďalší krok kvôli negácii.
                        Ten sme už ale rozobrali.}):
                    \begin{itemize}
                    \item $T \provable \neg B$ -- IP
                    \item $\provable \neg B \implies (B \implies C)$ --
                        z vety o neutrálnej formule
                    \item $T \provable B \implies C$ -- MP na prvé 2
                        formuly
                    \end{itemize}
                    V druhom prípade predpokladáme pravdivosť $C$,
                    t.j.
                    \begin{itemize}
                    \item $T \provable C$ -- IP
                    \item $\provable C \implies (B \implies C)$ -- A1
                    \item $T \provable B \implies C$ -- MP
                    \end{itemize}
                    Záver: ak platí
                    $\mathcal{M} \models B \implies C$, tak je formula
                    $B \implies C$ dokázateľná v $T$.
            \smallskip
            \item[$\Leftarrow:$] Uvažujeme, že
                $T \provable B \implies C$.
                Teória $T$ je úplná teória a $B \implies C$ je uzavretá.
                Pre každú uzavretú formulu platí jedna z možností
                $T \provable \neg B$ (potom $\mathcal{M} \models \neg B$ a sme
                hotoví) alebo $T \provable B$.
                Vtedy ale musí platiť $T \provable C$
                a teda $\mathcal{M} \models C$. Tým je tvrdenie dokázané.

                Ešte sa môžeme vrátiť k tomu, prečo platí $T \provable C$.
                Uvažujme totiž $T \provable \neg C$.
                \begin{itemize}
                \item $T \provable B \implies C$
                \item $T \provable B$ -- predpoklad
                \item $T \provable C$ -- MP
                \item $T \provable \neg C$ -- predpoklad a zároveň
                    spor s bezospornosťou teórie $T$.
                \end{itemize}
            \end{itemize}

        \item $A: (\forall x) B$. Pre každú
            inštanciu formuly $B$ tvrdenie platí.
            Pretože je teória úplná, môžu nastať 2 prípady:
            \begin{itemize}
            \item Platí $T\provable A$.
                Teda, $T \provable (\forall x) B$.
                Ďalej platí pre ľubovoľnú konštantu $c$,
                že je dokázateľné $\provable (\forall x) B \implies B_x[c]$
                -- axióma špecifikácie.
                Potom aj $T \provable B_x[c]$ (MP na axiómu
                špecifikácie). Lenže z IP dostávame
                $\forall c: \mathcal{M} \models B_x[c] \then 
                 \mathcal{M} \models (\forall x) B$.
            \smallskip
            \item Platí $T \provable \neg A$. Vtedy
                $T \provable (\exists x) \neg B$. Ďalej, keďže teória je
                Henkinovská, platí tiež 
                $T \provable (\exists x) \neg B \implies \neg B_x[c]$.
                Pomocou MP odvodíme
                $T \provable \neg B_x[c]$. Podobne ako v
                predchádzajúcom prípade máme
                $\mathcal{M} \models \neg B_x[c] \then
                 \mathcal{M} \not \models A$ (formula $B_x[c]$ je
                 nepravdivá a preto aj formula $(\forall x) B$ je
                 nepravdivá). Nuž ale potom
                 $\mathcal{M} \models \neg A$.
            \end{itemize}

        \end{itemize}
    \end{itemize}

    Ukázali sme, že pre uzavreté formuly vieme pomocou indukcie
    dokázať tvrdenie vety. Teraz, nech $A$ je ľubovoľná formula z teórie $T$.
    Pre ňu platí, že $T \provable A$ (predpoklad).
    Potrebujem dokázať, že $T \provable A \iff \mathcal{M} \models A$.
    Zoberiem si $A'$ -- uzáver formuly $A$.
    Na $A'$ sa vzťahuje naša indukcia a teda 
    $\mathcal{M} \models A' \iff T \provable A'$.
    Podľa vety o uzávere ale platí
    $\mathcal{M} \models A \iff  \mathcal{M} \models A'$ čo je 
    $\iff T \provable A'$ a z vety o uzávere $\iff T \provable A$.
    \\
\end{dokaz}

\noindent
Záver: Pre ľubovoľnú teóriu, ktorá je idealizovaná (Henkinova a
úplná), vieme zostrojiť model.

